Issue2408-error.agda:11,18-27
Set (lsuc (l a)) != Set₁
when checking that the expression Set (l a) has type Set₁
